module MainHelp (helpMain , helpMainPGF, helpMainFile, getContent) where

import PGF
import System.FilePath.Posix
import System.Process
import Syllogism
import TPTP
import Data.Maybe
import Structures
import Debug.Trace 

-- the input string should be on the form:
-- ( axiom + axiom + ... + axiom ) -> conclusion
-- and given in the input language
-- returns: Just (the answer från the theorem prover)
-- or Nothing if the input string could not be parsed
helpMain :: String -> Language -> IO (Maybe Answer)
helpMain input lang = do
   pgf    <- getPGF
   let mParsed = getContent lang pgf input
   case mParsed of
      []     -> return Nothing
      parsed -> do
         let axioms  = getTPTPofAxioms parsed
         let conc    = getTPTPofConclusion True parsed
         let concNeg = getTPTPofConclusion False parsed
         eOut    <- callEProver 0 (axioms ++ conc)
         eOutNeg <- callEProver 0 (axioms ++ concNeg)
         return (Just $ getAnswer eOut eOutNeg) 


-- used by clients that can provide the PGF
helpMainPGF :: String -> Language -> PGF -> IO (Maybe Answer)
helpMainPGF input lang pgf = do
   let mParsed = getContent lang pgf input
   case mParsed of
      []     -> return Nothing
      parsed -> do
         let axioms  = getTPTPofAxioms parsed
         let conc    = getTPTPofConclusion True parsed
         let concNeg = getTPTPofConclusion False parsed
         eOut    <- callEProver 0 (axioms ++ conc)
         eOutNeg <- callEProver 0 (axioms ++ concNeg)
         return (Just $ getAnswer eOut eOutNeg) 

-- for debugging purposes, does the same thing as helpMain
-- but creates two files with the given file-name:
-- filename.p and filename-neg.p
helpMainFile :: String -> Language -> FilePath -> IO (Maybe Answer)
helpMainFile input lang file = do
   pgf  <- getPGF
   let mParsed = getContent lang pgf input
   case mParsed of
      []     -> return Nothing
      parsed -> do
         let axioms  = getTPTPofAxioms parsed
         let conc    = getTPTPofConclusion True parsed
         let concNeg = getTPTPofConclusion False parsed
         writeFile (toP file) $ axioms ++ conc
         writeFile (toPNeg file) $ axioms ++ concNeg
         eOut    <- callEProverFile 0 $ toP file
         eOutNeg <- callEProverFile 0 $ toPNeg file
         return (Just $ getAnswer eOut eOutNeg) 


-- Datatype used to model EProver output
data EOutput = ProofFound | NoProofFound

getPGF :: IO PGF
getPGF = readPGF "../gf/Syllogism.pgf"

getTPTPofAxioms :: Syllogism -> String
getTPTPofAxioms syl = makeTPTPofAxioms $ init syl

getTPTPofConclusion :: Bool -> Syllogism -> String
getTPTPofConclusion b syl = makeTPTPofConclusion b $ last syl

getContent :: Language -> PGF -> String -> Syllogism
getContent lang pgf input = case parsed of
   [] -> []
   _  -> getSentences $ head parsed 
   where parsed = parse pgf lang (fromJust $ readType "Syllogism") input

--Calls EProver on the input with the given output level
callEProver :: Int -> String -> IO String
callEProver level input = readProcess "eprover" ["--tstp-in",getOutputFlag level] input


--Calls EProver on the input File with the given output level
callEProverFile :: Int -> FilePath -> IO String
callEProverFile level file = readProcess "eprover" ["--tstp-in",getOutputFlag level, file] []

getAnswer :: String -> String -> Answer
getAnswer eOut eOutNeg = case handleEOutputLevel0 eOut of
                  ProofFound -> case handleEOutputLevel0 eOutNeg of
                                  ProofFound -> AContr
                                  _          -> ATrue
                  _          -> case handleEOutputLevel0 eOutNeg of
                                  ProofFound -> AFalse
                                  _          -> AInconc

--Function for making a String with EProver output on level 0 into an EOutput
handleEOutputLevel0 :: String -> EOutput
handleEOutputLevel0 = proofFound . drop 2 . head . tail . lines

proofFound :: String -> EOutput
proofFound ('N':_) = NoProofFound
proofFound _       = ProofFound

getOutputFlag :: Int -> String
getOutputFlag = ("--output-level=" ++ ) . show

toP :: FilePath -> FilePath
toP = (++".p") . dropExtension

toPNeg :: FilePath -> FilePath
toPNeg = (++"-neg.p") . dropExtension


